

LEMMA

If x partially overlaps y and y is externally connected to z, then x is not part of z.
=============================
Step 1

? (all x (all y (all z (((po x y) & (ec y z)) => (~ (p x z))))))


> revsk
=============================
Step 2

? (((~ (po c786808 c786807)) v (~ (ec c786807 c786806))) v (~ (p c786808 c786806)))


> hypdisj
=============================
Step 3

? (~ (p c786808 c786806))

1. (ec c786807 c786806)
2. (po c786808 c786807)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var78 c786808)
|
|1. (p c786808 c786806)
|2. (ec c786807 c786806)
|3. (po c786808 c786807)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p Var81 c786808)
||
||1. (~ (c Var78 c786808))
||2. (p c786808 c786806)
||3. (ec c786807 c786806)
||4. (po c786808 c786807)
||
||> ((p Z X) <-- (~ (c (f781755 Z X Y) Z)))
||=============================
||Step 6
||
||? (~ (c (f781755 Var81 c786808 Var84) Var81))
||
||1. (~ (p Var81 c786808))
||2. (~ (c Var78 c786808))
||3. (p c786808 c786806)
||4. (ec c786807 c786806)
||5. (po c786808 c786807)
||
||> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|||=============================
|||Step 7
|||
|||? (p (f781772 Var87 Var91) Var87)
|||
|||1. (c (f781755 (f781772 Var87 Var91) c786808 Var84) (f781772 Var87 Var91))
|||2. (~ (p (f781772 Var87 Var91) c786808))
|||3. (~ (c Var78 c786808))
|||4. (p c786808 c786806)
|||5. (ec c786807 c786806)
|||6. (po c786808 c786807)
|||
|||> ((p (f781772 X Y) X) <-- (o X Y))
|||=============================
|||Step 8
|||
|||? (o Var87 Var91)
|||
|||1. (~ (p (f781772 Var87 Var91) Var87))
|||2. (c (f781755 (f781772 Var87 Var91) c786808 Var84) (f781772 Var87 Var91))
|||3. (~ (p (f781772 Var87 Var91) c786808))
|||4. (~ (c Var78 c786808))
|||5. (p c786808 c786806)
|||6. (ec c786807 c786806)
|||7. (po c786808 c786807)
|||
|||> ((o X Y) <-- (po X Y))
|||=============================
|||Step 9
|||
|||? (po Var87 Var91)
|||
|||1. (~ (o Var87 Var91))
|||2. (~ (p (f781772 Var87 Var91) Var87))
|||3. (c (f781755 (f781772 Var87 Var91) c786808 Var84) (f781772 Var87 Var91))
|||4. (~ (p (f781772 Var87 Var91) c786808))
|||5. (~ (c Var78 c786808))
|||6. (p c786808 c786806)
|||7. (ec c786807 c786806)
|||8. (po c786808 c786807)
|||
|||> hyp
||=============================
||Step 10
||
||? (~ (c (f781755 (f781772 c786808 c786807) c786808 Var84) c786808))
||
||1. (c (f781755 (f781772 c786808 c786807) c786808 Var84) (f781772 c786808 c786807))
||2. (~ (p (f781772 c786808 c786807) c786808))
||3. (~ (c Var78 c786808))
||4. (p c786808 c786806)
||5. (ec c786807 c786806)
||6. (po c786808 c786807)
||
||> ((~ (c (f781755 Y Z X) Z)) <-- (~ (p Y Z)))
||=============================
||Step 11
||
||? (~ (p (f781772 c786808 c786807) c786808))
||
||1. (c (f781755 (f781772 c786808 c786807) c786808 Var84) c786808)
||2. (c (f781755 (f781772 c786808 c786807) c786808 Var84) (f781772 c786808 c786807))
||3. (~ (p (f781772 c786808 c786807) c786808))
||4. (~ (c Var78 c786808))
||5. (p c786808 c786806)
||6. (ec c786807 c786806)
||7. (po c786808 c786807)
||
||> hyp
|=============================
|Step 12
|
|? (c (f781755 (f781772 c786808 c786807) Var101 Var102) (f781772 c786808 c786807))
|
|1. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) c786808))
|2. (p c786808 c786806)
|3. (ec c786807 c786806)
|4. (po c786808 c786807)
|
|> ((c (f781755 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 13
|
|? (~ (p (f781772 c786808 c786807) Var101))
|
|1. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) (f781772 c786808 c786807)))
|2. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) c786808))
|3. (p c786808 c786806)
|4. (ec c786807 c786806)
|5. (po c786808 c786807)
|
|> ((~ (p X Z)) <-- (p X Y) (~ (o Y Z)))
||=============================
||Step 14
||
||? (p (f781772 c786808 c786807) c786807)
||
||1. (p (f781772 c786808 c786807) Var101)
||2. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) (f781772 c786808 c786807)))
||3. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) c786808))
||4. (p c786808 c786806)
||5. (ec c786807 c786806)
||6. (po c786808 c786807)
||
||> ((p (f781772 X Y) Y) <-- (o X Y))
||=============================
||Step 15
||
||? (o c786808 c786807)
||
||1. (~ (p (f781772 c786808 c786807) c786807))
||2. (p (f781772 c786808 c786807) Var101)
||3. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) (f781772 c786808 c786807)))
||4. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) c786808))
||5. (p c786808 c786806)
||6. (ec c786807 c786806)
||7. (po c786808 c786807)
||
||> ((o X Y) <-- (po X Y))
||=============================
||Step 16
||
||? (po c786808 c786807)
||
||1. (~ (o c786808 c786807))
||2. (~ (p (f781772 c786808 c786807) c786807))
||3. (p (f781772 c786808 c786807) Var101)
||4. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) (f781772 c786808 c786807)))
||5. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) c786808))
||6. (p c786808 c786806)
||7. (ec c786807 c786806)
||8. (po c786808 c786807)
||
||> hyp
|=============================
|Step 17
|
|? (~ (o c786807 Var101))
|
|1. (p (f781772 c786808 c786807) Var101)
|2. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) (f781772 c786808 c786807)))
|3. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) c786808))
|4. (p c786808 c786806)
|5. (ec c786807 c786806)
|6. (po c786808 c786807)
|
|> ((~ (o X Y)) <-- (ec X Y))
|=============================
|Step 18
|
|? (ec c786807 Var101)
|
|1. (o c786807 Var101)
|2. (p (f781772 c786808 c786807) Var101)
|3. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) (f781772 c786808 c786807)))
|4. (~ (c (f781755 (f781772 c786808 c786807) Var101 Var102) c786808))
|5. (p c786808 c786806)
|6. (ec c786807 c786806)
|7. (po c786808 c786807)
|
|> hyp
=============================
Step 19

? (~ (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806))

1. (p c786808 c786806)
2. (ec c786807 c786806)
3. (po c786808 c786807)

> ((~ (c (f781755 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 20

? (~ (p (f781772 c786808 c786807) c786806))

1. (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806)
2. (p c786808 c786806)
3. (ec c786807 c786806)
4. (po c786808 c786807)

> ((~ (p X Y)) <-- (p X Z) (~ (o Y Z)))
|=============================
|Step 21
|
|? (p (f781772 c786808 c786807) c786807)
|
|1. (p (f781772 c786808 c786807) c786806)
|2. (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806)
|3. (p c786808 c786806)
|4. (ec c786807 c786806)
|5. (po c786808 c786807)
|
|> ((p (f781772 X Y) Y) <-- (o X Y))
|=============================
|Step 22
|
|? (o c786808 c786807)
|
|1. (~ (p (f781772 c786808 c786807) c786807))
|2. (p (f781772 c786808 c786807) c786806)
|3. (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806)
|4. (p c786808 c786806)
|5. (ec c786807 c786806)
|6. (po c786808 c786807)
|
|> ((o X Y) <-- (po X Y))
|=============================
|Step 23
|
|? (po c786808 c786807)
|
|1. (~ (o c786808 c786807))
|2. (~ (p (f781772 c786808 c786807) c786807))
|3. (p (f781772 c786808 c786807) c786806)
|4. (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806)
|5. (p c786808 c786806)
|6. (ec c786807 c786806)
|7. (po c786808 c786807)
|
|> hyp
=============================
Step 24

? (~ (o c786806 c786807))

1. (p (f781772 c786808 c786807) c786806)
2. (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806)
3. (p c786808 c786806)
4. (ec c786807 c786806)
5. (po c786808 c786807)

> ((~ (o Y X)) <-- (~ (p (f781772 Y X) Y)))
=============================
Step 25

? (~ (p (f781772 c786806 c786807) c786806))

1. (o c786806 c786807)
2. (p (f781772 c786808 c786807) c786806)
3. (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806)
4. (p c786808 c786806)
5. (ec c786807 c786806)
6. (po c786808 c786807)

> ((~ (p X Z)) <-- (p X Y) (~ (o Y Z)))
|=============================
|Step 26
|
|? (p (f781772 c786806 c786807) c786807)
|
|1. (p (f781772 c786806 c786807) c786806)
|2. (o c786806 c786807)
|3. (p (f781772 c786808 c786807) c786806)
|4. (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806)
|5. (p c786808 c786806)
|6. (ec c786807 c786806)
|7. (po c786808 c786807)
|
|> ((p (f781772 X Y) Y) <-- (o X Y))
|=============================
|Step 27
|
|? (o c786806 c786807)
|
|1. (~ (p (f781772 c786806 c786807) c786807))
|2. (p (f781772 c786806 c786807) c786806)
|3. (o c786806 c786807)
|4. (p (f781772 c786808 c786807) c786806)
|5. (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806)
|6. (p c786808 c786806)
|7. (ec c786807 c786806)
|8. (po c786808 c786807)
|
|> hyp
=============================
Step 28

? (~ (o c786807 c786806))

1. (p (f781772 c786806 c786807) c786806)
2. (o c786806 c786807)
3. (p (f781772 c786808 c786807) c786806)
4. (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806)
5. (p c786808 c786806)
6. (ec c786807 c786806)
7. (po c786808 c786807)

> ((~ (o X Y)) <-- (ec X Y))
=============================
Step 29

? (ec c786807 c786806)

1. (o c786807 c786806)
2. (p (f781772 c786806 c786807) c786806)
3. (o c786806 c786807)
4. (p (f781772 c786808 c786807) c786806)
5. (c (f781755 (f781772 c786808 c786807) c786806 Var102) c786806)
6. (p c786808 c786806)
7. (ec c786807 c786806)
8. (po c786808 c786807)

> hyp


LEMMA

Partial overlap implies overlap.
=============================
Step 1

? (all x (all y ((po x y) => (o x y))))


> revsk
=============================
Step 2

? ((~ (po c792037 c792036)) v (o c792037 c792036))


> hypdisj
=============================
Step 3

? (o c792037 c792036)

1. (po c792037 c792036)

> ((o X Y) <-- (po X Y))
=============================
Step 4

? (po c792037 c792036)

1. (~ (o c792037 c792036))
2. (po c792037 c792036)

> hyp


LEMMA

Overlap implies connection.
=============================
Step 1

? (all x (all y ((o x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (o c797322 c797321)) v (c c797322 c797321))


> hypdisj
=============================
Step 3

? (c c797322 c797321)

1. (o c797322 c797321)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var48 c797321)
|
|1. (~ (c c797322 c797321))
|2. (o c797322 c797321)
|
|> ((p Z X) <-- (~ (c (f792069 Z X Y) Z)))
|=============================
|Step 5
|
|? (~ (c (f792069 Var48 c797321 Var51) Var48))
|
|1. (~ (p Var48 c797321))
|2. (~ (c c797322 c797321))
|3. (o c797322 c797321)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 6
||
||? (p (f792086 Var57 Var54) Var54)
||
||1. (c (f792069 (f792086 Var57 Var54) c797321 Var51) (f792086 Var57 Var54))
||2. (~ (p (f792086 Var57 Var54) c797321))
||3. (~ (c c797322 c797321))
||4. (o c797322 c797321)
||
||> ((p (f792086 X Y) Y) <-- (o X Y))
||=============================
||Step 7
||
||? (o Var57 Var54)
||
||1. (~ (p (f792086 Var57 Var54) Var54))
||2. (c (f792069 (f792086 Var57 Var54) c797321 Var51) (f792086 Var57 Var54))
||3. (~ (p (f792086 Var57 Var54) c797321))
||4. (~ (c c797322 c797321))
||5. (o c797322 c797321)
||
||> hyp
|=============================
|Step 8
|
|? (~ (c (f792069 (f792086 c797322 c797321) c797321 Var51) c797321))
|
|1. (c (f792069 (f792086 c797322 c797321) c797321 Var51) (f792086 c797322 c797321))
|2. (~ (p (f792086 c797322 c797321) c797321))
|3. (~ (c c797322 c797321))
|4. (o c797322 c797321)
|
|> ((~ (c (f792069 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p (f792086 c797322 c797321) c797321))
|
|1. (c (f792069 (f792086 c797322 c797321) c797321 Var51) c797321)
|2. (c (f792069 (f792086 c797322 c797321) c797321 Var51) (f792086 c797322 c797321))
|3. (~ (p (f792086 c797322 c797321) c797321))
|4. (~ (c c797322 c797321))
|5. (o c797322 c797321)
|
|> hyp
=============================
Step 10

? (c c797322 (f792086 c797322 c797321))

1. (~ (c c797322 c797321))
2. (o c797322 c797321)

> ((c Y X) <-- (c X Y))
=============================
Step 11

? (c (f792086 c797322 c797321) c797322)

1. (~ (c c797322 (f792086 c797322 c797321)))
2. (~ (c c797322 c797321))
3. (o c797322 c797321)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 12
|
|? (p (f792086 c797322 Var71) c797322)
|
|1. (~ (c (f792086 c797322 c797321) c797322))
|2. (~ (c c797322 (f792086 c797322 c797321)))
|3. (~ (c c797322 c797321))
|4. (o c797322 c797321)
|
|> ((p (f792086 X Y) X) <-- (o X Y))
|=============================
|Step 13
|
|? (o c797322 Var71)
|
|1. (~ (p (f792086 c797322 Var71) c797322))
|2. (~ (c (f792086 c797322 c797321) c797322))
|3. (~ (c c797322 (f792086 c797322 c797321)))
|4. (~ (c c797322 c797321))
|5. (o c797322 c797321)
|
|> hyp
=============================
Step 14

? (c (f792086 c797322 c797321) (f792086 c797322 c797321))

1. (~ (c (f792086 c797322 c797321) c797322))
2. (~ (c c797322 (f792086 c797322 c797321)))
3. (~ (c c797322 c797321))
4. (o c797322 c797321)

> ((c X X) <--)


LEMMA

External connection implies connection.
=============================
Step 1

? (all x (all y ((ec x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (ec c802663 c802662)) v (c c802663 c802662))


> hypdisj
=============================
Step 3

? (c c802663 c802662)

1. (ec c802663 c802662)

> ((c X Y) <-- (ec X Y))
=============================
Step 4

? (ec c802663 c802662)

1. (~ (c c802663 c802662))
2. (ec c802663 c802662)

> hyp


LEMMA

Parthood transports connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c808062 c808061)) v (~ (c c808060 c808062))) v (c c808060 c808061))


> hypdisj
=============================
Step 3

? (c c808060 c808061)

1. (c c808060 c808062)
2. (p c808062 c808061)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c808061)
|
|1. (~ (c c808060 c808061))
|2. (c c808060 c808062)
|3. (p c808062 c808061)
|
|> hyp
=============================
Step 5

? (c c808060 c808062)

1. (~ (c c808060 c808061))
2. (c c808060 c808062)
3. (p c808062 c808061)

> hyp


LEMMA

Split x,z into disconnection or connection.
=============================
Step 1

? (all x (all y (all z (((po x y) & (ec y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (po c813617 c813616)) v (~ (ec c813616 c813615))) v ((dc c813617 c813615) v (c c813617 c813615)))


> hypdisj
=============================
Step 3

? (c c813617 c813615)

1. (~ (dc c813617 c813615))
2. (ec c813616 c813615)
3. (po c813617 c813616)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c813617 c813615))

1. (~ (c c813617 c813615))
2. (~ (dc c813617 c813615))
3. (ec c813616 c813615)
4. (po c813617 c813616)

> hyp


LEMMA

In the connected case, x,z are ec or po or z is part of x.
=============================
Step 1

? (all x (all y (all z ((((po x y) & (ec y z)) & (c x z)) => (((ec x z) v (po x z)) v (p z x))))))


> revsk
=============================
Step 2

? ((((~ (po c819438 c819437)) v (~ (ec c819437 c819436))) v (~ (c c819438 c819436))) v (((ec c819438 c819436) v (po c819438 c819436)) v (p c819436 c819438)))


> hypdisj
=============================
Step 3

? (p c819436 c819438)

1. (~ (po c819438 c819436))
2. (~ (ec c819438 c819436))
3. (c c819438 c819436)
4. (ec c819437 c819436)
5. (po c819438 c819437)

> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||=============================
||Step 4
||
||? (o c819438 c819436)
||
||1. (~ (p c819436 c819438))
||2. (~ (po c819438 c819436))
||3. (~ (ec c819438 c819436))
||4. (c c819438 c819436)
||5. (ec c819437 c819436)
||6. (po c819438 c819437)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 5
|||
|||? (c c819438 c819436)
|||
|||1. (~ (o c819438 c819436))
|||2. (~ (p c819436 c819438))
|||3. (~ (po c819438 c819436))
|||4. (~ (ec c819438 c819436))
|||5. (c c819438 c819436)
|||6. (ec c819437 c819436)
|||7. (po c819438 c819437)
|||
|||> hyp
||=============================
||Step 6
||
||? (~ (ec c819438 c819436))
||
||1. (~ (o c819438 c819436))
||2. (~ (p c819436 c819438))
||3. (~ (po c819438 c819436))
||4. (~ (ec c819438 c819436))
||5. (c c819438 c819436)
||6. (ec c819437 c819436)
||7. (po c819438 c819437)
||
||> hyp
|=============================
|Step 7
|
|? (~ (p c819438 c819436))
|
|1. (~ (p c819436 c819438))
|2. (~ (po c819438 c819436))
|3. (~ (ec c819438 c819436))
|4. (c c819438 c819436)
|5. (ec c819437 c819436)
|6. (po c819438 c819437)
|
|> ((~ (p X Z)) <-- (po X Y) (ec Y Z))
||=============================
||Step 8
||
||? (po c819438 Var37)
||
||1. (p c819438 c819436)
||2. (~ (p c819436 c819438))
||3. (~ (po c819438 c819436))
||4. (~ (ec c819438 c819436))
||5. (c c819438 c819436)
||6. (ec c819437 c819436)
||7. (po c819438 c819437)
||
||> hyp
|=============================
|Step 9
|
|? (ec c819437 c819436)
|
|1. (p c819438 c819436)
|2. (~ (p c819436 c819438))
|3. (~ (po c819438 c819436))
|4. (~ (ec c819438 c819436))
|5. (c c819438 c819436)
|6. (ec c819437 c819436)
|7. (po c819438 c819437)
|
|> hyp
=============================
Step 10

? (~ (po c819438 c819436))

1. (~ (p c819436 c819438))
2. (~ (po c819438 c819436))
3. (~ (ec c819438 c819436))
4. (c c819438 c819436)
5. (ec c819437 c819436)
6. (po c819438 c819437)

> hyp


LEMMA

Converse parthood plus failure of forward parthood gives inverse proper part.
=============================
Step 1

? (all x (all y (((p y x) & (~ (p x y))) => (pp-1 x y))))


> revsk
=============================
Step 2

? (((~ (p c825868 c825869)) v (p c825869 c825868)) v (pp-1 c825869 c825868))


> hypdisj
=============================
Step 3

? (pp-1 c825869 c825868)

1. (~ (p c825869 c825868))
2. (p c825868 c825869)

> ((pp-1 Y X) <-- (pp X Y))
=============================
Step 4

? (pp c825868 c825869)

1. (~ (pp-1 c825869 c825868))
2. (~ (p c825869 c825868))
3. (p c825868 c825869)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 5
|
|? (p c825868 c825869)
|
|1. (~ (pp c825868 c825869))
|2. (~ (pp-1 c825869 c825868))
|3. (~ (p c825869 c825868))
|4. (p c825868 c825869)
|
|> hyp
=============================
Step 6

? (~ (p c825869 c825868))

1. (~ (pp c825868 c825869))
2. (~ (pp-1 c825869 c825868))
3. (~ (p c825869 c825868))
4. (p c825868 c825869)

> hyp


LEMMA

Inverse proper part splits into tangential or non-tangential inverse proper part.
=============================
Step 1

? (all x (all y ((pp-1 x y) => ((tpp-1 x y) v (ntpp-1 x y)))))


> revsk
=============================
Step 2

? ((~ (pp-1 c832451 c832450)) v ((tpp-1 c832451 c832450) v (ntpp-1 c832451 c832450)))


> hypdisj
=============================
Step 3

? (ntpp-1 c832451 c832450)

1. (~ (tpp-1 c832451 c832450))
2. (pp-1 c832451 c832450)

> ((ntpp-1 Y X) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c832450 c832451)

1. (~ (ntpp-1 c832451 c832450))
2. (~ (tpp-1 c832451 c832450))
3. (pp-1 c832451 c832450)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f825980 Z X Y) Z)))
|=============================
|Step 5
|
|? (pp c832450 c832451)
|
|1. (~ (ntpp c832450 c832451))
|2. (~ (ntpp-1 c832451 c832450))
|3. (~ (tpp-1 c832451 c832450))
|4. (pp-1 c832451 c832450)
|
|> ((pp Y X) <-- (pp-1 X Y))
|=============================
|Step 6
|
|? (pp-1 c832451 c832450)
|
|1. (~ (pp c832450 c832451))
|2. (~ (ntpp c832450 c832451))
|3. (~ (ntpp-1 c832451 c832450))
|4. (~ (tpp-1 c832451 c832450))
|5. (pp-1 c832451 c832450)
|
|> hyp
=============================
Step 7

? (~ (ec (f825980 c832450 c832451 Var44) c832450))

1. (~ (ntpp c832450 c832451))
2. (~ (ntpp-1 c832451 c832450))
3. (~ (tpp-1 c832451 c832450))
4. (pp-1 c832451 c832450)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 8
||
||? (pp c832450 Var50)
||
||1. (ec (f825980 c832450 c832451 Var44) c832450)
||2. (~ (ntpp c832450 c832451))
||3. (~ (ntpp-1 c832451 c832450))
||4. (~ (tpp-1 c832451 c832450))
||5. (pp-1 c832451 c832450)
||
||> ((pp Y X) <-- (pp-1 X Y))
||=============================
||Step 9
||
||? (pp-1 Var50 c832450)
||
||1. (~ (pp c832450 Var50))
||2. (ec (f825980 c832450 c832451 Var44) c832450)
||3. (~ (ntpp c832450 c832451))
||4. (~ (ntpp-1 c832451 c832450))
||5. (~ (tpp-1 c832451 c832450))
||6. (pp-1 c832451 c832450)
||
||> hyp
|=============================
|Step 10
|
|? (ec (f825980 c832450 c832451 Var44) c832451)
|
|1. (ec (f825980 c832450 c832451 Var44) c832450)
|2. (~ (ntpp c832450 c832451))
|3. (~ (ntpp-1 c832451 c832450))
|4. (~ (tpp-1 c832451 c832450))
|5. (pp-1 c832451 c832450)
|
|> ((ec (f825980 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 11
||
||? (~ (ntpp c832450 c832451))
||
||1. (~ (ec (f825980 c832450 c832451 Var44) c832451))
||2. (ec (f825980 c832450 c832451 Var44) c832450)
||3. (~ (ntpp c832450 c832451))
||4. (~ (ntpp-1 c832451 c832450))
||5. (~ (tpp-1 c832451 c832450))
||6. (pp-1 c832451 c832450)
||
||> hyp
|=============================
|Step 12
|
|? (pp c832450 c832451)
|
|1. (~ (ec (f825980 c832450 c832451 Var44) c832451))
|2. (ec (f825980 c832450 c832451 Var44) c832450)
|3. (~ (ntpp c832450 c832451))
|4. (~ (ntpp-1 c832451 c832450))
|5. (~ (tpp-1 c832451 c832450))
|6. (pp-1 c832451 c832450)
|
|> ((pp Y X) <-- (pp-1 X Y))
|=============================
|Step 13
|
|? (pp-1 c832451 c832450)
|
|1. (~ (pp c832450 c832451))
|2. (~ (ec (f825980 c832450 c832451 Var44) c832451))
|3. (ec (f825980 c832450 c832451 Var44) c832450)
|4. (~ (ntpp c832450 c832451))
|5. (~ (ntpp-1 c832451 c832450))
|6. (~ (tpp-1 c832451 c832450))
|7. (pp-1 c832451 c832450)
|
|> hyp
=============================
Step 14

? (~ (tpp c832450 c832451))

1. (ec (f825980 c832450 c832451 Var44) c832450)
2. (~ (ntpp c832450 c832451))
3. (~ (ntpp-1 c832451 c832450))
4. (~ (tpp-1 c832451 c832450))
5. (pp-1 c832451 c832450)

> ((~ (tpp Y X)) <-- (~ (tpp-1 X Y)))
=============================
Step 15

? (~ (tpp-1 c832451 c832450))

1. (tpp c832450 c832451)
2. (ec (f825980 c832450 c832451 Var44) c832450)
3. (~ (ntpp c832450 c832451))
4. (~ (ntpp-1 c832451 c832450))
5. (~ (tpp-1 c832451 c832450))
6. (pp-1 c832451 c832450)

> hyp


LEMMA

Split dc/c. In connected case use Lemma7. If p(z,x), use Lemma1 to eliminate p(x,z), yielding pp-1(x,z), then split to tpp-1 or ntpp-1.
=============================
Step 1

? (all x (all y (all z (((po x y) & (ec y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp-1 x z)) v (ntpp-1 x z))))))


> revsk
=============================
Step 2

? (((~ (po c839186 c839185)) v (~ (ec c839185 c839184))) v (((((dc c839186 c839184) v (ec c839186 c839184)) v (po c839186 c839184)) v (tpp-1 c839186 c839184)) v (ntpp-1 c839186 c839184)))


> hypdisj
=============================
Step 3

? (ntpp-1 c839186 c839184)

1. (~ (tpp-1 c839186 c839184))
2. (~ (po c839186 c839184))
3. (~ (ec c839186 c839184))
4. (~ (dc c839186 c839184))
5. (ec c839185 c839184)
6. (po c839186 c839185)

> ((ntpp-1 X Y) <-- (pp-1 X Y) (~ (tpp-1 X Y)))
|=============================
|Step 4
|
|? (pp-1 c839186 c839184)
|
|1. (~ (ntpp-1 c839186 c839184))
|2. (~ (tpp-1 c839186 c839184))
|3. (~ (po c839186 c839184))
|4. (~ (ec c839186 c839184))
|5. (~ (dc c839186 c839184))
|6. (ec c839185 c839184)
|7. (po c839186 c839185)
|
|> ((pp-1 X Y) <-- (p Y X) (~ (p X Y)))
||=============================
||Step 5
||
||? (p c839184 c839186)
||
||1. (~ (pp-1 c839186 c839184))
||2. (~ (ntpp-1 c839186 c839184))
||3. (~ (tpp-1 c839186 c839184))
||4. (~ (po c839186 c839184))
||5. (~ (ec c839186 c839184))
||6. (~ (dc c839186 c839184))
||7. (ec c839185 c839184)
||8. (po c839186 c839185)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c839186 c839184)
||||
||||1. (~ (p c839184 c839186))
||||2. (~ (pp-1 c839186 c839184))
||||3. (~ (ntpp-1 c839186 c839184))
||||4. (~ (tpp-1 c839186 c839184))
||||5. (~ (po c839186 c839184))
||||6. (~ (ec c839186 c839184))
||||7. (~ (dc c839186 c839184))
||||8. (ec c839185 c839184)
||||9. (po c839186 c839185)
||||
||||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||||=============================
|||||Step 7
|||||
|||||? (c c839186 c839184)
|||||
|||||1. (~ (o c839186 c839184))
|||||2. (~ (p c839184 c839186))
|||||3. (~ (pp-1 c839186 c839184))
|||||4. (~ (ntpp-1 c839186 c839184))
|||||5. (~ (tpp-1 c839186 c839184))
|||||6. (~ (po c839186 c839184))
|||||7. (~ (ec c839186 c839184))
|||||8. (~ (dc c839186 c839184))
|||||9. (ec c839185 c839184)
|||||10. (po c839186 c839185)
|||||
|||||> ((c X Y) <-- (~ (dc X Y)))
|||||=============================
|||||Step 8
|||||
|||||? (~ (dc c839186 c839184))
|||||
|||||1. (~ (c c839186 c839184))
|||||2. (~ (o c839186 c839184))
|||||3. (~ (p c839184 c839186))
|||||4. (~ (pp-1 c839186 c839184))
|||||5. (~ (ntpp-1 c839186 c839184))
|||||6. (~ (tpp-1 c839186 c839184))
|||||7. (~ (po c839186 c839184))
|||||8. (~ (ec c839186 c839184))
|||||9. (~ (dc c839186 c839184))
|||||10. (ec c839185 c839184)
|||||11. (po c839186 c839185)
|||||
|||||> hyp
||||=============================
||||Step 9
||||
||||? (~ (ec c839186 c839184))
||||
||||1. (~ (o c839186 c839184))
||||2. (~ (p c839184 c839186))
||||3. (~ (pp-1 c839186 c839184))
||||4. (~ (ntpp-1 c839186 c839184))
||||5. (~ (tpp-1 c839186 c839184))
||||6. (~ (po c839186 c839184))
||||7. (~ (ec c839186 c839184))
||||8. (~ (dc c839186 c839184))
||||9. (ec c839185 c839184)
||||10. (po c839186 c839185)
||||
||||> hyp
|||=============================
|||Step 10
|||
|||? (~ (p c839186 c839184))
|||
|||1. (~ (p c839184 c839186))
|||2. (~ (pp-1 c839186 c839184))
|||3. (~ (ntpp-1 c839186 c839184))
|||4. (~ (tpp-1 c839186 c839184))
|||5. (~ (po c839186 c839184))
|||6. (~ (ec c839186 c839184))
|||7. (~ (dc c839186 c839184))
|||8. (ec c839185 c839184)
|||9. (po c839186 c839185)
|||
|||> ((~ (p X Z)) <-- (po X Y) (ec Y Z))
||||=============================
||||Step 11
||||
||||? (po c839186 Var55)
||||
||||1. (p c839186 c839184)
||||2. (~ (p c839184 c839186))
||||3. (~ (pp-1 c839186 c839184))
||||4. (~ (ntpp-1 c839186 c839184))
||||5. (~ (tpp-1 c839186 c839184))
||||6. (~ (po c839186 c839184))
||||7. (~ (ec c839186 c839184))
||||8. (~ (dc c839186 c839184))
||||9. (ec c839185 c839184)
||||10. (po c839186 c839185)
||||
||||> hyp
|||=============================
|||Step 12
|||
|||? (ec c839185 c839184)
|||
|||1. (p c839186 c839184)
|||2. (~ (p c839184 c839186))
|||3. (~ (pp-1 c839186 c839184))
|||4. (~ (ntpp-1 c839186 c839184))
|||5. (~ (tpp-1 c839186 c839184))
|||6. (~ (po c839186 c839184))
|||7. (~ (ec c839186 c839184))
|||8. (~ (dc c839186 c839184))
|||9. (ec c839185 c839184)
|||10. (po c839186 c839185)
|||
|||> hyp
||=============================
||Step 13
||
||? (~ (po c839186 c839184))
||
||1. (~ (p c839184 c839186))
||2. (~ (pp-1 c839186 c839184))
||3. (~ (ntpp-1 c839186 c839184))
||4. (~ (tpp-1 c839186 c839184))
||5. (~ (po c839186 c839184))
||6. (~ (ec c839186 c839184))
||7. (~ (dc c839186 c839184))
||8. (ec c839185 c839184)
||9. (po c839186 c839185)
||
||> hyp
|=============================
|Step 14
|
|? (~ (p c839186 c839184))
|
|1. (~ (pp-1 c839186 c839184))
|2. (~ (ntpp-1 c839186 c839184))
|3. (~ (tpp-1 c839186 c839184))
|4. (~ (po c839186 c839184))
|5. (~ (ec c839186 c839184))
|6. (~ (dc c839186 c839184))
|7. (ec c839185 c839184)
|8. (po c839186 c839185)
|
|> ((~ (p X Z)) <-- (po X Y) (ec Y Z))
||=============================
||Step 15
||
||? (po c839186 Var61)
||
||1. (p c839186 c839184)
||2. (~ (pp-1 c839186 c839184))
||3. (~ (ntpp-1 c839186 c839184))
||4. (~ (tpp-1 c839186 c839184))
||5. (~ (po c839186 c839184))
||6. (~ (ec c839186 c839184))
||7. (~ (dc c839186 c839184))
||8. (ec c839185 c839184)
||9. (po c839186 c839185)
||
||> hyp
|=============================
|Step 16
|
|? (ec c839185 c839184)
|
|1. (p c839186 c839184)
|2. (~ (pp-1 c839186 c839184))
|3. (~ (ntpp-1 c839186 c839184))
|4. (~ (tpp-1 c839186 c839184))
|5. (~ (po c839186 c839184))
|6. (~ (ec c839186 c839184))
|7. (~ (dc c839186 c839184))
|8. (ec c839185 c839184)
|9. (po c839186 c839185)
|
|> hyp
=============================
Step 17

? (~ (tpp-1 c839186 c839184))

1. (~ (ntpp-1 c839186 c839184))
2. (~ (tpp-1 c839186 c839184))
3. (~ (po c839186 c839184))
4. (~ (ec c839186 c839184))
5. (~ (dc c839186 c839184))
6. (ec c839185 c839184)
7. (po c839186 c839185)

> hyp
